es:event_system{i:l}, l:IdLnk, tg:Id, e:es-E(es).
(es-isrcv(es; e))
 (es-lnk(es; e) = l)
 (es-tag(es; e) = tg)
 (es-kind(es; e) = rcv(l,tg)  Knd) 

latex

Definitions	es-isrcv(es; e), es-lnk(es; e), es-tag(es; e), Knd, <a, b>, rcv(l,tg), tag(k), lnk(k), b, isrcv(k), es-E(es), event_system{i:l}, atom{$n:n}, Id, x:A  B(x), sqequal(s; t), prop{i:l}, s = t, IdLnk, sq_type(T), guard(T), P  Q, es-kind(es; e), x:A. B(x), t  T
Lemmas	es-kind wf, isrcv-implies, IdLnk sq, IdLnk wf, Id sq, Id wf, event system wf, es-E wf, isrcv wf, assert wf, lnk wf, tagof wf